package proj2;

import java.util.*;


/**
 * This object parses a string in First order logic and returns an object with the result
 * @author Draz
 *
 */
public class FOLParser {
	
	public String initial;
	public String normalized;
	public Expression expression;
	public LinkedList<String> predicates;
	public LinkedList<String> variables;
	public boolean trace = false;
	public String[] conectors = {"AND","OR","IMP","EQV"};
	public Hashtable<String, Expression> mgu;
	private static String ALL = "ALL";
	private static String EXT = "EXT";
	@SuppressWarnings("unused")
	private static String AND = "AND";
	@SuppressWarnings("unused")
	private static String OR = "OR";
	private static String NOT = "NOT";
	
	FOLParser(String s) {
		initial = s.replace("  ", " ").trim();
		int[] arr = parenthesis("("+initial+")");
		if(arr[2]!=-1)
			expression = parse(initial);
		else
			expression = null;
	}
	FOLParser() {
		
	}
	

	private boolean hasConector(String str) {
		if(str.isEmpty()) return false;
		for (String c : conectors) {
			if(str.contains(c)){
				return true;
			}
		}
		return false;
	}
	@SuppressWarnings("unused")
	private boolean isNot(String str) {
		return str.contains(NOT);
	}
	private boolean isQuantifier(String s) {
		return (s.contains(ALL) || s.contains(EXT));
	}
	private boolean isPredicate(String p) {
		return (p.length()==0)?false:Character.isUpperCase(p.charAt(0));
	}
	
	
	/**
	 * This method detects parenthesis in a string and returns the start and end index
	 * of the first matching pair ignoring any parenthesis in between
	 * @param s String to parse
	 * @return index of start and end of parenthesis, -1 if no parenthesis or wrong match, the third output is -1 if error, 0 if no para, and 1 if succecful parse
	 */
	private int[] parenthesis(String s){
		return parenthesis(s, 0);
	}
	/**
	 * This method detects parenthesis in a string and returns the start and end index
	 * of the first matching pair ignoring any parenthesis in between
	 * @param s String to parse
	 * @param i start of parsing
	 * @return index of start and end of parenthesis, -1 if no parenthesis or wrong match
	 */
	private int[] parenthesis(String s, int i){
		int j,k,m,n,l=0,r=0,v=0;
		j = s.indexOf('(', i);
		k = j;
		n=j;
		m=j;
		if(j!=-1) {
			v=1;
			l=1;
			do {
				m = s.indexOf(')',m+1);
				k = m;
				if(m==-1){
					v=-1;
					break;
				} else {
					r++;
				}
				
				n = s.indexOf('(',n+1);
				if(n!=-1 && n<m){
					l++;
				}				
			} while (l!=r);
		}
		
		return new int[]{j,k,v};
	}
	/**
	 * parses the arguments of an FOL function
	 * @param arg
	 * @return a String list of the function arguments
	 */
	private LinkedList<String> parseArgs(String arg) {
		int m,n;
		String str;
		int[] arr;
		LinkedList<String> args = new LinkedList<String>();
		m = -1;
		do {
			n = arg.indexOf(",",m+1);
			
			if(n==-1) {
				str = arg.substring(m+1);
				args.addLast(str);
				if(trace){
					System.out.print(", "+str);
				}
				break;
			}
			str = arg.substring(m+1,n).trim();
			arr = parenthesis(str);
			if(arr[0]!=-1 && arr[1]==-1) {
				do {
					m=n;
					n = arg.indexOf(",", n+1);
					str+= ", "+arg.substring(m+1,n).trim();
					arr = parenthesis(str);
				} while (arr[1]==-1);
			}
			if (trace) System.out.print(", "+str);
			args.addLast(str);
			m = n;
		} while(m!=-1);
		
		return args;
	}
	/**
	 * parses an FOL statement and turns it into an expression object
	 * @param s
	 * @return
	 */
	public Expression parse(String s){
		

		if(trace) System.out.println("Parsing: "+s);
		
		if(s.equals("") || s.equals(" ")) return null;
		
		String str="",name="";
		Expression exp;
		
		int startPara = 0,endPara=0,m,startCon;
		int[] arr = parenthesis(s); //get the next parenthesis
		startPara = arr[0]; //start of parenthesis
		endPara = arr[1]; //endOf parenthesis
		
		if(startPara==0 && (endPara+1)==s.length()) { //statement is needlessly wrapped in parenthesis
			if(trace) System.out.println("Ignored parenthesis");
			return parse(s.substring(startPara+1, endPara).trim());
		}
		
		startCon = indexOfConnector(s); //start of connector (and, or, etc...)
		
		
		if(arr[2]==1 && endPara>startCon || startCon==-1) { //there is no connector outside the parenthesis
			str = (startPara==-1)?s.trim():s.substring(0,startPara).trim(); //the quantifier or predicate, or empty
			
			m = str.indexOf(' ', 0);
			if(m!=-1) { //space before parenthesis
				name = str.substring(0,m);
			} else { //space after
				name = str;
				if(startPara==-1){ //no parenthesis and no spaces implies that this is the only atom in the string
					if(trace) System.out.println("Parsed: "+name+"  as "+(isPredicate(name)?"Constant":"veriable"));
					return new Expression(name);
				}
			}
			
			exp = new Expression(name);
			
			if(isQuantifier(str)) {
				String[] quantify = str.substring(m+1).split(" ");
				for (String q : quantify) {
					exp.addVariable(q);
				}
				exp.addArgument(parse(s.substring(startPara+1, endPara+1)));
			} else if (isPredicate(str)){
				if(endPara!=-1){
					String arg = s.substring(startPara+1, endPara).trim();
					if(trace) System.out.print("Parsed: "+name+" as predicate with args");
					LinkedList<String> args = parseArgs(arg);
					if(trace) System.out.println();
					
					for (String a : args) {
						if(trace) System.out.print("\t");
						exp.addArgument(parse(a.trim()));
					}
					
				} else {
					if(trace) System.out.println("Parsed: "+name+"  as Constant");
				}
			}
		} else { //there is a connector outside parenthesis this statement
			//it has a connector
			m = startCon+3; //all connectors are 3 characters
			name = s.substring(startCon,m).trim();
			String left = s.substring(0, startCon).trim();
			String right = s.substring(m).trim();
			if(trace) {
				if(trace) System.out.println("Parsing "+name+" Connector with Arguments: ["+left+"] left and ["+right+"] right");
			}
			exp = new Expression(name);
			exp.addArgument(parse(left));
			exp.addArgument(parse(right));
		}
		
		
		return exp;
		
	}
	private int indexOfConnector(String s) { return indexOfConnector(s, 0); }
	/**
	 * finds the first appearance of a connector in a string starting position i
	 * and returns the connector's position in the string
	 * @param s String to search in
	 * @param i start index
	 * @return The start index position of the connector in the String
	 */
	private int indexOfConnector(String s, int i) {
		if(!hasConector(s)) return -1;
		int startPara = 0,endPara=0,startCon=0, ci;
		
		
		//System.out.println("searching for connector in "+s.substring(i));
		
		for (String c : conectors) {
			ci = s.indexOf(c, i);
			if(ci!=-1 && ci>startCon) startCon = ci;
		}
		//closest is now max
		for (String c : conectors) {
			ci = s.indexOf(c, i);
			if(ci!=-1 && ci<startCon) startCon = ci;
		}
		
		int[] arr = parenthesis(s); //get the next parenthesis
		startPara = arr[0]; //start of parenthesis
		endPara = arr[1]; //endOf parenthesis
		//case we have parenthesis
		if((arr[2]==1 && endPara>startCon && startPara<startCon)) {
			//System.out.println("parsed up to "+s.substring(0,endPara+1));
			return endPara + indexOfConnector(s.substring(endPara+1)) +1;
		}
		//System.out.println("returning index of "+s.substring(startCon,startCon+3));
		return startCon;
	}


	/**
	 * @param args
	 */
	public static void main(String[] args) {
		System.out.println("Parsing FOL");
		

		// The parser can take the following syntax
		// These test cases are examples of things the parser would take
		String[] test = {
				"", 				//an empty string => will evaluate to null
				" ",				// an empty space character => will evaluate to null
				"(())",				//empty parenthesis, which will be ignored leaving an empty string evaluating to null
				"x", 				// a word/character that starts with a lower case => will evaluate this as a variable expression
				"Constant",			//a word/character that starts with an upper case => will be evaluate as a constant expression
				"P(x)",				// a word/character that starts with an upper case followed by parenthesis => will evaluate into a function that takes what ever is in the parenthesis ass arguments
				"Hello(World)",		// an other example of a function that has a constant as an argument
				"(P(x))",			// in this case the parenthesis will be ignored and the function will evaluate what's inside
				"Hello(x,y,z)",		// an example of passing multiple arguments		
				"World( Hi(x) ,Hello(y))",			//arguments can be other functions that the parser can evaluate
				"World( x ,Hello(y))",				//the arguments can be different expression
				"World( w, Hi(x, y) ,Hello(z))", 	//another test
				//this part highlights connectors
				//a connector is an AND for and, OR for or, IMP for implication, and EQV for equivalence
				"x AND y OR x AND y", // you can have as many connectors as you want
				"Hello(x) AND World (x)", //they can parse expressions
				"(x) IMP (z AND y)", //you can use parenthesis
				"(x AND y ) EQV (z OR w)", //decide on precedence using parenthesis
				//this part highlights quantifiers
				//A quantifier is either an ALL for for all quantifier, or EXT for existential quantifier
				"ALL x (Hello(x))" //this is an example, anything between the parenthesis and the ALL are considered variables the rest is evaluated as an expression
				};
		
		String[][] toUnify = {
				{"A", "B"},
				{"A", "A"},
				{"y", "x"},
				{"x", "A"},
				{"A", "x"},
				{"x", "P(x)"},
				{"P(x)", "P(A)"},
				{"P(x,G(x),G(F(A)))", "P(F(u),v,v)"},
				{"P(A,y,F(y))","P(z,z,u)"},
				{"F(x,G(x),x)","F(G(u),G(G(z)),z)"},
				};
		FOLParser fol = new FOLParser();

		
		//System.out.print("\nFOL Parsed: ");
		
		//System.out.println(fol.listify());
		int tst = 8;
		System.out.println("\nMGU: "+fol.unify(toUnify[tst][0], toUnify[tst][1]));
	}
	
	public String listify(){
		return (expression!=null)?expression.listify():"Expression was not parssed it may evaluate to an empty expression";
	}
	public Hashtable<String, Expression> unify(String e1, String e2) {
		Expression E1 = parse(e1);
		Expression E2 = parse(e2);
		System.out.println("Unifiying "+E1+" with "+E2);
		System.out.println("Listifyed "+E1.listify()+" and "+E2.listify());
		return unify(E1,E2);
	}
	public Hashtable<String, Expression> unify(Expression e1, Expression e2)
	{
		
	    if (e1.isConstant() && e2.isConstant())
	    {
	        if (e1.name.equals(e2.name)) {
	        	System.out.println("matched "+e1);
	        	return new Hashtable<String, Expression>();
	        }
	        System.out.println("Could not match "+e1+" "+e2);
	        return null;
	    }

	    if (e1.isVariable())
	    {
	       if( e2.occurs(e1.name)) {
	    	   System.out.println("Can't e1 with e2 unify "+e1+" ocures in "+e2);
	    	   return null;
	       }
	       
	       Hashtable<String, Expression> u = new Hashtable<String, Expression>();
		   u.put(e1.name, e2);
		   System.out.println(e1+"(e1) is a var returning "+u);
	       return u;
	    }
	    
	    if (e2.isVariable())
	    {
	       if (e1.occurs(e2.name))  {
	    	   System.out.println("Can't unify e2 with e1 "+e2+" ocures in "+e1);
	    	   return null;
	       }
	       Hashtable<String, Expression> u = new Hashtable<String, Expression>();
		   u.put(e2.name, e1);
		   System.out.println(e2+"(e2) is a var returning "+u);
	       return u;
	    }
	    
	    //is same function
	    if(!e1.name.equals(e2.name) || e1.args.size() != e2.args.size()) return null;
	    
	    System.out.println("both e1 and e2 are lists");
	    
	    Expression HE1 = e1.args.getFirst();
	    Expression HE2 = e2.args.getFirst();
	    
	    System.out.println("unifying "+HE1+" "+HE2);
	    
	    Hashtable<String, Expression> SUB1 = unify(HE1, HE2);
	    if (SUB1==null) return null;
	    
	    System.out.println("applying unification to the rest of the list");
	    
	    Expression TE1 = e1.removeAndApply(SUB1);
	    Expression TE2 = e2.removeAndApply(SUB1);
	    
	    System.out.println("unifying remaning expression "+TE1+" and "+TE2);
	    
	    Hashtable<String, Expression> SUB2 = unify(TE1, TE2);
	    if (SUB2==null) return null;
	    
	    return composition(SUB1, SUB2);

	}

	/**
	 * applies u2 to u1 and vice versa then joins them to form a general unifier
	 * { X/Y, W/Z }, { V/X }, { a/V, f(b)/W } are together equivalent to { a/Y, f(b)/Z }
	 * @param u1
	 * @param u2
	 * @return
	 */
	private Hashtable<String, Expression> composition(
			Hashtable<String, Expression> u1,
			Hashtable<String, Expression> u2) {
		
		Hashtable<String, Expression> u = new Hashtable<String, Expression>();
		for (String key : u2.keySet()) {
			if(u2.get(key).isVariable()) {
				for(Expression e : u1.values()) {
					if(e.isVariable() && e.name.equals(u2.get(key).name)) {
						u.put(key, e);
					}
				}
			} else {
				u.put(key, u2.get(key));
			}
		}
		
		for (String key : u1.keySet()) {
			if(u1.get(key).isVariable()) {
				for(Expression e : u2.values()) {
					if(e.isVariable() && e.name.equals(u1.get(key).name)) {
						u.put(key, e);
					}
				}
			} else {
				u.put(key, u1.get(key));
			}
		}
		
		return u;
	}

}

class Expression {
	static int UID = 1;
	String name;
	LinkedList<Expression> args;
	LinkedList<String> quantify;
	
	Expression(String n){
		name = n;
		args = new LinkedList<Expression>();
		quantify = new LinkedList<String>();
	}
	Expression(Expression e){
		this(e.name);
		if(!e.isAtom()){
			for (Expression exp : e.args) {
				addArgument(new Expression(exp));
			}
			for (String q : e.quantify) {
				addVariable(q);
			}
		}
	}
	/**
	 * returns whether this expression is an Atom
	 * @return
	 */
	public boolean isAtom(){
		return args.isEmpty();
	}
	/**
	 * checks is this atom expression is s a constant
	 * @return
	 */
	public boolean isConstant(){
		return isAtom() && Character.isUpperCase(name.charAt(0));
	}
	/**
	 * checks is this atom expression is s a variable
	 * @return
	 */
	public boolean isVariable(){
		return isAtom() && Character.isLowerCase(name.charAt(0));
	}
	/**
	 * returns whether this expression is a quantifier
	 * @return
	 */
	public boolean isQuantifier(){
		return !quantify.isEmpty();
	}
	/**
	 * returns whether this expression is an Atom
	 * @return
	 */
	public boolean hasArgs(){
		return !args.isEmpty();
	}
	/**
	 * This method adds an expression, that is be an atom or another expression, that this expression applied to it
	 * @param exp
	 */
	public void addArgument(Expression exp){
		if(exp!=null) args.add(exp);
	}
	/**
	 * This method adds a variable to quantify if this Expression is a Quantifier
	 * @param q
	 */
	public void addVariable(String q){
		if(q!=null) quantify.add(q);
	}
	/**
	 * outputs a string with the listified version of this expression for unification
	 * @return
	 */
	public String listify() {
		String exp;
		if(isAtom()){
			exp = name;
		} else {
			exp =  "( "+name+" ";
			if(isQuantifier()){
				exp+= " ( ";
				for (String v : quantify) {
					exp+= v+" ";
				}
				exp+=") ";
			}
			for (Expression e : args) {
				exp+= e.listify()+" ";
			}
			exp+=")";
		}
		return exp;
	}
	/**
	 * removes the first argument in the expression and applies the unification in u on the rest
	 * @param u a general unifier
	 * @return a new expression that the unification was applied on
	 */
	public Expression removeAndApply(Hashtable<String, Expression> u) {
		args.removeFirst();
		return this.apply(u);
	}
	/**
	 * applies a general unifier to an expression
	 * @param u
	 * @return an expression with the unification applied on it
	 */
	public Expression apply(Hashtable<String, Expression> u){
		if(hasArgs()){
			for (int i=0;i<args.size();i++) {
				args.set(i, args.get(i).apply(u));
			}
		} else if(isVariable()) {
			Expression e = u.get(name);
			if(e!=null){
				return new Expression(e);
			}
		}
		return  new Expression(this);
	}
	public Hashtable<String, Expression> contains(String var) {
		Hashtable<String, Expression> u = new Hashtable<String, Expression>(); 
		if(isAtom()){
			u.put(var, this); 
		} else {
			
		}
		return u;
	}
	public boolean occurs(String var){
		
		if(isConstant()) return false;
		if(isVariable()) {
			return name.equals(var);
		}
		for (Expression e : args) {
			if(e.occurs(var)) {
				return true;
			}
		}
		return false;
	}
	
	public String toString(){
		String s="";
		s+= name;
		if(isQuantifier()) {
			s+=" ";
			for (String v : quantify) {
				s+= v+" ";
			}
		}
		if(hasArgs()){
			s+="(";
			String st = "";
			for (Expression e : args) {
				st+= ", "+e;
			}
			s+= st.substring(2) +")";
		}
		return s;
	}
	/**
	 * converts an EQV expression to 2 ANDed Implications
	 * @return an expression
	 */
	public Expression deEQV() {
		Expression e = new Expression("AND"),
				imp1 = new Expression("IMP"),
				imp2 = new Expression("IMP");
		
		imp1.addArgument(new Expression(args.getFirst()));
		imp1.addArgument(new Expression(args.getLast()));
		
		imp2.addArgument(new Expression(args.getLast()));
		imp2.addArgument(new Expression(args.getFirst()));
		
		e.addArgument(imp1);
		e.addArgument(imp2);
		
		return e;
	}
	
	/**
	 * converts an IMP expression to not the precedent ORed with the antecedent
	 * @return and expression
	 */
	public Expression deIMP() {
		Expression e = new Expression("OR"),
				not = new Expression("NOT");
		
		not.addArgument(new Expression(args.getFirst()));
		
		e.addArgument(not);
		e.addArgument(args.getLast());
		
		return e;
	}
	
	/**
	 * 
	 * @return an expression who's not has been pushed to the atoms
	 */
	public Expression deNOT() {
		
		Expression ex = args.getFirst();
		
		if(ex.isAtom()) return this;
		
		if(ex.isQuantifier()){
			Expression e = new Expression(this);
			if(ex.name.equals("ALL")) {
				e.name = "EXT";
			} else {
				e.name = "ALL";
			}
			ex = e.args.poll();
			e.quantify = ex.quantify;
			ex.quantify = null;
			ex.name = "NOT";
			e.addArgument(ex.deNOT());
			return e;
		} else if(ex.name.equals("AND")){
			Expression e = new Expression("OR"),
					not1 = new Expression("NOT"),
					not2 = new Expression("NOT");
			
			not1.addArgument(new Expression(ex.args.getFirst()));
			not2.addArgument(new Expression(ex.args.getLast()));
			
			e.addArgument(not1.deNOT());
			e.addArgument(not2.deNOT());
			return e;
		} else if(ex.name.equals("OR")){
			Expression e = new Expression("AND"),
					not1 = new Expression("NOT"),
					not2 = new Expression("NOT");
			
			not1.addArgument(ex.args.getFirst());
			not2.addArgument(ex.args.getLast());
			
			e.addArgument(not1.deNOT());
			e.addArgument(not2.deNOT());
			return e;
		} else if(ex.name.equals("NOT")){
			return new Expression(ex.args.getFirst());
		} else { //it's a function;
			return this;
		}
		
	}
	
	public Expression rename() {
		// TODO Auto-generated method stub
		return null;
	}
	
}
